Nuprl Lemma : sublist-same-last 11,40
T:Type, L, L':(T List).
((null(L)))
 no_repeats(T;L)
 ((null(L')))
 L'  L
 (last(L)  L')
 (last(L') = last(L)  T) 
latex

Definitionss = t, x:AB(x), x:A. B(x), Type, type List, A, no_repeats(T;l), L1  L2, (x  l), x before y  l, left + right, P  Q, Void, P  Q, b, False, x:A  B(x), x:A. B(x), increasing(f;k), a < b, null(as), , t  T, l[i], x:A.B(x), Top, S  T, last(L), P & Q, P  Q, P  Q, {T}
Lemmasl before sublist, no repeats-sublist, last-not-before, l member wf, sublist wf, no repeats wf, not wf, assert wf, null wf3, member wf, top wf, l tricotomy, last wf, last member

origin